1. Technical Field
The present invention generally relates to sequential equivalence checking and in particular to using sequential equivalence checking to verify performance of clock gating designs.
2. Description of the Related Art
Sequential equivalence checking (SEC) solutions are increasingly being used to perform a wide variety of verification tasks. These verification tasks range from the most common application of SEC proving that sequential transformations late in the design phase do not change design functionality to proving that partial good self-test fencing structures work correctly. SEC performs a true sequential check of input/output equivalence, hence unlike more prevalent combinational equivalence checking solutions, the equivalence check is not limited to operating on designs with 1:1 state element pairings; however, with this generality in equivalence checking comes with higher computational expense of the SEC algorithms. For scalability of SEC, it is often required that a substantial number of internal equivalence points exist between the two designs.
One or more SEC solutions can be used to verification of designs that have one or more portions shut off for one or more periods of time (e.g., during periods of inactivity) while other portions of the design are in operation. This is known as clock gating, and clock gating can be used to conserve power, which power consumption can be a factor in designing modern processors. In clock gating verification, one goal is to verify the control logic that implements clock gating, while other functionality of a design being clock gated are not important; However, clock gating introduces verification complexity as the logic for turning off the clocks adds new states and increases the complexity of the design. One approach for verifying a clock gating transformation is to perform a sequential equivalence check between the “design with clock gating enabled” and the “design with clock gating disabled”. The sequential equivalence check is performed to verify that the two designs are input/output equivalent under the “care” (as opposed to “don't care”) conditions when the design is required to produce valid outputs, but this sequential equivalence check is very complex since there are virtually no equivalent internal gates across the two designs being verified. For instance, the logic is equivalent only under the “care” conditions. Due to the lack of internal equivalence, equivalence checking algorithms tend to become intractable since no internal points may be merged to simplify the overall input/output equivalence check.